package parser.util;

import java.util.ArrayList;
import java.util.Collection;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;

import parser.astgen.NodeFactory;
import parser.sablecc.analysis.AttrEvalException;
import project.Project;
import uml2.kernel.DataType;
import uml2.kernel.Enumeration;
import uml2.kernel.Operation;
import uml2.kernel.Property;
import uml2.kernel.Type;
import uml2.kernel.TypedElement;
import uml2.kernel.UmlClass;
import uml2.ocl2.BagType;
import uml2.ocl2.BooleanLiteralExp;
import uml2.ocl2.CallExp;
import uml2.ocl2.CollectionItem;
import uml2.ocl2.CollectionKind;
import uml2.ocl2.CollectionKindEnum;
import uml2.ocl2.CollectionLiteralExp;
import uml2.ocl2.CollectionLiteralPart;
import uml2.ocl2.CollectionRange;
import uml2.ocl2.CollectionType;
import uml2.ocl2.IfExp;
import uml2.ocl2.IntegerLiteralExp;
import uml2.ocl2.IterateExp;
import uml2.ocl2.IteratorExp;
import uml2.ocl2.LetExp;
import uml2.ocl2.LoopExp;
import uml2.ocl2.OclExpression;
import uml2.ocl2.OperationCallExp;
import uml2.ocl2.OrderedSetType;
import uml2.ocl2.PropertyCallExp;
import uml2.ocl2.RealLiteralExp;
import uml2.ocl2.SequenceType;
import uml2.ocl2.SetType;
import uml2.ocl2.StringLiteralExp;
import uml2.ocl2.TupleLiteralExp;
import uml2.ocl2.TupleLiteralPart;
import uml2.ocl2.TupleType;
import uml2.ocl2.Variable;
import uml2.ocl2.VariableExp;
import exceptions.ConstraintException;
import facade.UserFacade;
import facade.kernel.DataTypeFacade;

/**
 * This class performs the type check of the elements that appear in the OCL and UML Metamodels. These elements
 * are used for the construction of the constraints in the repository from the abstract syntax tree.
 * Operations named 'evaluate' must never be called directly. Use typecheck instead.
 * 
 * It extends ReflectiveVisitor class, wich implements a Visitor Pattern that does not need to modify the basic element classes
 * to visit. 
 * 
 * @author Antonio Villegas
 *
 */

public class TypeCheck extends ReflectiveVisitor {

	UserFacade uf;
	DataTypeFacade df;
	NodeFactory factory;
	Utility ut;
	public static final boolean verbose = false;
	// Lists for make easier the operations identification
	LinkedList aritmeticops;
	LinkedList logicalops;
	LinkedList collectops;
	LinkedList relationalops;
	LinkedList additionalops;
	// Lists for make easier the types identification
	LinkedList primitivetypes;
	
	private static final int NO_MULTIPLICITY = -2;
	
	
	public TypeCheck(Project p, NodeFactory n) {
		super("evaluate");
		this.uf = new UserFacade(p);
		this.df = new DataTypeFacade(p);
		this.factory = n;
		this.ut = new Utility(this.uf, p);
		ut.setTypeCheck(this);
		initlists();
	}
	
	/**
	 * This method initialize the Lists explained before with the correct elements
	 */
	private void initlists() {
		// init relationalops
		this.relationalops = new LinkedList();
		this.relationalops.add(">");
		this.relationalops.add("<");
		this.relationalops.add(">=");
		this.relationalops.add("<=");
		this.relationalops.add("=");
		this.relationalops.add("<>");
		// init logicalops
		this.logicalops = new LinkedList();
		this.logicalops.add("and");
		this.logicalops.add("or");
		this.logicalops.add("xor");
		this.logicalops.add("implies");
		this.logicalops.add("not");
		// init aritmeticops
		this.aritmeticops = new LinkedList();
		this.aritmeticops.add("+");
		this.aritmeticops.add("-");
		this.aritmeticops.add("*");
		this.aritmeticops.add("/");
		// init additionalops
		this.additionalops = new LinkedList();
		this.additionalops.add("abs");
		this.additionalops.add("floor");
		this.additionalops.add("round");
		this.additionalops.add("max");
		this.additionalops.add("min");
		this.additionalops.add("div");
		this.additionalops.add("mod");
		this.additionalops.add("size");
		this.additionalops.add("concat");
		this.additionalops.add("substring");
		this.additionalops.add("toInteger");
		this.additionalops.add("toReal");
		// init collectops
		this.collectops = new LinkedList();
		this.collectops.add("size");
		this.collectops.add("isEmpty");
		this.collectops.add("notEmpty");
		this.collectops.add("includes");
		this.collectops.add("excludes");
		this.collectops.add("count");
		this.collectops.add("includesAll");
		this.collectops.add("excludesAll");
		this.collectops.add("sum");
		this.collectops.add("product");
		this.collectops.add("union");
		this.collectops.add("intersection");
		this.collectops.add("including");
		this.collectops.add("excluding");
		this.collectops.add("symmetricDifference");
		this.collectops.add("flatten");
		this.collectops.add("asSet");
		this.collectops.add("asOrderedSet");
		this.collectops.add("asSequence");
		this.collectops.add("asBag");
		this.collectops.add("append");
		this.collectops.add("prepend");
		this.collectops.add("insertAt");
		this.collectops.add("subOrderedSet");
		this.collectops.add("subSequence");
		this.collectops.add("at");
		this.collectops.add("indexOf");
		this.collectops.add("first");
		this.collectops.add("last");
		this.collectops.add("ñ");
		
		// init primitivetypes
		this.primitivetypes = new LinkedList();
		this.primitivetypes.add("Integer");
		this.primitivetypes.add("Real");
		this.primitivetypes.add("Boolean");
		this.primitivetypes.add("String");
	}
	
	 /** Evaluates the type of a TypedElement.
     * During this evaluation, the types of the subexpressions are determined as well (if not already evaluated before.)
     * @param te the TypedElement
     * @throws WellFormednessException
     * @return the type
     */
	public Type typecheck (TypedElement te) throws WellFormednessException , AttrEvalException{
		Type t = te.getType();
		// if the element has no type, we use the visitor pattern to get it
		if (t == null) {
			try {
				visit(te);
			} catch (NoSuchMethodException e) {
				//some  method is missing in the visitor implementation
                e.printStackTrace();
			} catch (java.lang.reflect.InvocationTargetException e){
                Throwable nestedException = e.getTargetException();
                if(nestedException instanceof WellFormednessException){
                    throw (WellFormednessException) nestedException;
                }
                else if (nestedException instanceof AttrEvalException){
                	throw (AttrEvalException) nestedException;
                }
                else {
                    nestedException.printStackTrace();
                }
            }
		}
		t = te.getType();
		return t;
	}


	/*====================*
	 *   OCL Expressions  *
	 *====================*/
	
	 /** Never call directly. Use {@link #typecheck typecheck} instead. 
	 * @throws AttrEvalException */ 
    public void evaluate(IfExp exp) throws AttrEvalException {
        OclExpression cond = exp.getCondition();
        // condition of the if expression must not be null
        if(cond==null){
            throw new WellFormednessException(exp, WellFormednessException.EC_NO_CONDITION);
        }
        // condition must be boolean
        if(!typecheck(cond).equals(uf.findDataTypeByName("Boolean"))){
            throw new WellFormednessException(exp, WellFormednessException.EC_CONDITION_NOT_BOOL);
        }
        
        OclExpression thenExp = exp.getThenExpression();
        if(thenExp==null){
            throw new WellFormednessException(exp, WellFormednessException.EC_NO_THEN_EXP);
        }
        
        OclExpression elseExp = exp.getElseExpression();
        if(elseExp==null){
            throw new WellFormednessException(exp, WellFormednessException.EC_NO_ELSE_EXP);
        }
        // the type of an IfExp is the common supertype of the then and the else branch
        exp.setType(commonSuperType(typecheck(thenExp),typecheck(elseExp)));
    }

    /** Never call directly. Use {@link #typecheck typecheck} instead. 
     * @throws AttrEvalException */  
    public void evaluate(LetExp exp) throws AttrEvalException{
        OclExpression inExp = exp.getIn();
        if(inExp==null){
            throw new WellFormednessException(exp, WellFormednessException.EC_NO_IN_EXP);
        }

        Variable v = exp.getVariable();
        if(v==null){
            throw new WellFormednessException(v, WellFormednessException.EC_NO_VARIABLE);
        }

        Type inType = typecheck(inExp);
        if(inExp instanceof PropertyCallExp) inType = ut.createTypeForPCE((PropertyCallExp) inExp);
        
        exp.setType(inType);
    }

    
    public void evaluate(VariableExp ve) throws AttrEvalException {
    	Variable v = ve.getReferredVariable();
    	ve.setType(v.getType());
    }
    /** 
     * Evaluate the type of an iterator expression. This type basically depends on the name of the iterator expression.
     * 
     * Never call directly. Use {@link #typecheck typecheck} instead. 
     * @throws AttrEvalException */      
    public void evaluate(IteratorExp exp) throws AttrEvalException{
        
    	// evaluate the iterator variables
    	evaluateIteratorTypes(exp); //we have to do that, BEFORE we evaluate the type of the body!
        
    	Type type = null; // variable to return
    	
    	// we get source's type, elements' type of the source collection and body's type
        Type srcType = evaluateSourceType(exp);
        Type elementType = ((CollectionType)srcType).getElementType();
        Type bodyType = evaluateBodyType(exp);
        
        String name = exp.getName(); // it can be forAll, select, reject, any, exists, isUnique, one and collect
        
        //iterators that need a boolean body expression ...
        Type bool = uf.findDataTypeByName("Boolean");
        if(name.equals("exists")||name.equals("forAll")||name.equals("select")||name.equals("reject")||name.equals("any")){
            if(!bodyType.equals(bool)){
                throw new WellFormednessException(exp, WellFormednessException.EC_BODY_NOT_BOOL);
            }
        }
        
        //iterators that need a body expression type with the "<" operation defined
        if (name.equals("sortedBy")) {
        	if (! this.hasMinOperationDefined(bodyType)) {
                throw new WellFormednessException(exp, WellFormednessException.EC_BODY_TYPE_WITHOUT_MINUS_OP_DECLARED);
            } 
        }
        
        //iterators with boolean result ...
        if(name.equals("exists")||name.equals("forAll")||name.equals("isUnique")||name.equals("one")){
            type=bool;
        }
        // iterator any -> result type is element's type
        else if(name.equals("any")){
            type=elementType;
        }
        // iterators select and reject  -> result type is equals to source type
        else if(name.equals("select")||name.equals("reject")){
            type=srcType;
        }
        // iterator sortedBy -> result type is orderedset or sequence
        else if(name.equals("sortedBy")){
            if(srcType instanceof SetType || srcType instanceof OrderedSetType){
            	type = ut.newCollectionType("OrderedSet", elementType);
            }
            else{
            	type = ut.newCollectionType("Sequence", elementType);
            } 
        }
        // iterator collectNested
        else if(name.equals("collectNested")){
            //collect without flattening
            if(srcType instanceof SequenceType || srcType instanceof OrderedSetType){
            	SequenceType st = (SequenceType) factory.createNode("SequenceType");
            	st.setName("Sequence("+bodyType.getName()+")");
            	st.setElementType(bodyType);
                type = st;
            } else {
            	BagType bt = (BagType) factory.createNode("BagType");
            	bt.setName("Bag("+bodyType.getName()+")");
            	bt.setElementType(bodyType);
                type = bt;
            }
        }
        // iterator collect
        else if(name.equals("collect")){
        	// Firstly, obtain the ElementType
        	Type resultElementType;
            if (bodyType instanceof CollectionType){
                resultElementType = ((CollectionType) bodyType).getElementType();
            } else {
                resultElementType = bodyType;
            }
            // Now, create the correct result type
            if(srcType instanceof SequenceType || srcType instanceof OrderedSetType){
            	SequenceType st = (SequenceType) factory.createNode("SequenceType");
            	st.setName("Sequence("+resultElementType.getName()+")");
            	st.setElementType(resultElementType);
                type = st;
            } else /* source instanceof Set or Bag */ {
            	BagType bt = (BagType) factory.createNode("BagType");
            	bt.setName("Bag("+resultElementType.getName()+")");
            	bt.setElementType(resultElementType);
                type = bt;
            }
        }
        else{
            //some unknown iterator expression
            throw new WellFormednessException(exp, WellFormednessException.EC_UNKNOWN_ITERATOR_EXP);
        }
        exp.setType(type);
    }

    public void evaluateInitializedVariable(Variable myAst) throws AttrEvalException {
		OclExpression initExp = myAst.getInitExpression();
        if(initExp==null){
            throw new WellFormednessException(myAst, WellFormednessException.EC_NO_INIT_EXP);
        }
        Type initExpType = typecheck(initExp);
        initExpType = ut.getCorrectType(initExp);
        
        if(myAst.getType() == null){
        	if (verbose) System.out.println("TC:Ponemos el tipo "+initExpType.getName());
            myAst.setType(initExpType);
        }
        else if(!this.existsCompatibility(myAst.getType(), initExpType)){
            throw new WellFormednessException(myAst, WellFormednessException.EC_WRONG_VAR_INIT_TYPE);     
        }
        if (verbose) System.out.println("Tipo de la variable "+myAst.getName()+" es "+myAst.getType().getName());
	}
    

	/*===============================*
     *  Auxiliar Methods for LoopExp *
     *===============================*/
    public void evaluate(IterateExp exp) throws AttrEvalException {
    	evaluateIteratorTypes(exp); //we have to do that, BEFORE we evaluate the type of the body!

    	Type bodyType = evaluateBodyType(exp);
    	Variable result = exp.getResult();
 

    	if(result==null){
    		throw new WellFormednessException(exp, WellFormednessException.EC_NO_ACCUMUMLATOR_VAR);
    	}

    	OclExpression init = result.getInitExpression(); 
    	if(init == null){
    		throw new WellFormednessException(result, WellFormednessException.EC_NO_INIT_EXP);
    	}

    	Type initType = typecheck(init);
    	if (init instanceof PropertyCallExp) {
    		PropertyCallExp pce = (PropertyCallExp) init;
    		initType = ut.newCollectionType(pce, pce.getType());
    	}
    	Type resultType = typecheck(result);


    	if(resultType == null){
    		//       //there variable declaration has no explicit type
    		//       //=> take the supertype of init-expression and body-expression
    		//        resultType=initType.commonSuperType(bodyType);
    		//        result.setType(resultType);
    		throw new WellFormednessException(result, WellFormednessException.EC_ACCU_VAR_NO_TYPE);
    	} else {
    		if(!existsCompatibility(resultType, initType)){
    			throw new WellFormednessException(result, WellFormednessException.EC_WRONG_VAR_INIT_TYPE);
    		} 
    		if(!existsCompatibility(resultType, bodyType)){
    			System.out.println("Accumulator type: "+resultType.getName());
    			System.out.println("Body type: "+bodyType.getName());
    			throw new WellFormednessException(exp, WellFormednessException.EC_WRONG_BODY_TYPE);
    		}
    	}
    	
    	//Issues: WFRs [2],[3]
    	exp.setType(resultType);
    }

    
    /**
     * checks wheter the iterator variables have the right type. if their type is still undefined, 
     * it is set to the element type of the collection type of the source expression 
     */
    private void evaluateIteratorTypes(LoopExp exp) throws AttrEvalException{
        Type srcType = evaluateSourceType(exp);
        if (verbose) System.out.println(">>>>>Tipo del collection source es "+srcType.getName());
        if(!(srcType instanceof CollectionType)){
            throw new WellFormednessException(exp, WellFormednessException.EC_SRC_NOT_COLLECTION);
        }
        Type elementType = ((CollectionType)srcType).getElementType();
        if (verbose) System.out.println(">>>>>Tipo del elemento del collection source es "+elementType.getName());
        
        if(exp.getIterator().size()==0){
            throw new WellFormednessException(exp, WellFormednessException.EC_NO_ITERATOR_VARS);
        }
        
        Iterator it = exp.getIterator().iterator();
        while(it.hasNext()){
            Variable vd = (Variable) it.next();
            if(vd.getInitExpression()!=null){
                throw new WellFormednessException(vd, WellFormednessException.EC_ILLEGAL_ITERATOR_VAR_INIT);
            }
            Type vdType = vd.getType();
            if( vdType == null ){
                vd.setType(elementType);  
            } else {
                //type of iterator variable explicitly stated...
                if(!vdType.equals(elementType)){
                    //...but wrong
                	if (verbose) System.out.println(">>>>>Tipo de la variable "+vdType.getName());
                    throw new WellFormednessException(vd, WellFormednessException.EC_ITERATOR_VAR_WRONG_TYPE);
                }
            }
        }       
    }
    /**
     * evaluates the type of the source expression from a call expression
     */
    private Type evaluateSourceType(CallExp exp) throws AttrEvalException{
        OclExpression source = exp.getSource();
        if(source == null){
            throw new WellFormednessException(exp, WellFormednessException.EC_NO_SOURCE_EXP);
        }
        if (source instanceof PropertyCallExp) {
        	PropertyCallExp pce = (PropertyCallExp) source;
        	int resulttype = ut.computeResultTypeOfNavigation(pce);
        	return ut.createTypeForCollectionPCE(resulttype, pce.getType());
        }
        return typecheck(source);
    }    
    /**
     * evaluate the type of the body expression from a LoopExp
     */
    private Type evaluateBodyType(LoopExp exp) throws AttrEvalException{
        OclExpression body = exp.getBody();
        if(body==null){
            throw new WellFormednessException(exp, WellFormednessException.EC_NO_BODY_EXP);
        }
        return typecheck(body);
    }
    /**
     * evaluate the type of the body expression from a LoopExp.
     * return true if the type constains < operation defined
     */
    private boolean hasMinOperationDefined(Type bodyType) {
		//TODO this operation must be redefined with a more general behaviour
    	if (bodyType.getName().equals("Integer")|| bodyType.getName().equals("Real")) return true;
		return false;
	}


	
	/*=====================*
	 *   Call Expressions  *
	 *=====================*/
	/** Never call directly. Use {@link #typecheck typecheck} instead. 
	 * @throws WellFormednessException */   
	public void evaluate (PropertyCallExp pce) throws WellFormednessException {
		Property p = pce.getReferredProperty();
		if(p==null){
            //a source expression must exist
            throw new WellFormednessException(pce, WellFormednessException.EC_NO_REF_PROP);
        }
		if (p.getType()==null) {
		    //a source expression must have type
            throw new WellFormednessException(p, WellFormednessException.EC_NO_SRCTYPE);
		}
		if (verbose) System.out.println("Property "+p.getName()+" has "+p.getType().getName()+" as a type");
		
		// The type of a PopertyCallExp is the type of the property
		pce.setType(p.getType());
	}
	

	/** Never call directly. Use {@link #typecheck typecheck} instead. 
	 * @throws AttrEvalException 
	 * @throws ConstraintException */   
	public void evaluate (OperationCallExp oce) throws AttrEvalException, ConstraintException {
		Type t = null; // SetType variable
		
		OclExpression source = (OclExpression) oce.getSource();
		if (verbose) System.out.println("Inside evaluation of Operation CallExp");
		// Maybe it is correct
		// An IfExp cannot be an operationcall's source
		//if (source instanceof IfExp) 
		//	throw new WellFormednessException(source,WellFormednessException.EC_ILLEGAL_SOURCE);
		
		// Operation must not be null
		Operation op = oce.getReferredOperation();
        if(op == null){
            throw new WellFormednessException(oce, WellFormednessException.EC_NO_OPERATION);
        }
		
		// Case 1. Aritmetic and Logic Operation
		if (aritmeticops.contains(op.getName()) ||
			relationalops.contains(op.getName())||
			logicalops.contains(op.getName())     ) {
			
			// Get the right side operand
			OclExpression argument = null;
			if (oce.getArgument().size()==1) {
				Object[] array = oce.getArgument().toArray();
				argument = (OclExpression) array[0];
			}
			
			t = evaluateArithmeticAndLogicBinaryOpCall(source, op, argument);
		}
		// Case 2. Collection Operation
		else if (collectops.contains(op.getName())) {
			Collection params = oce.getArgument();
			t = evaluateCollectionOpCall(source, op, params);
		}
		// Case 3. Class Operation
		else {
			// TO-DO implementation
			if (verbose) System.out.println("Not implemented");
		}
		
		
		if (t==null) throw new WellFormednessException(oce,WellFormednessException.EC_UNKNOWN);
		else oce.setType(t);
	}
	
	
	
	/*=====================*
	 * Literal Expressions *
	 *=====================*/
	/** Never call directly. Use {@link #typecheck typecheck} instead. */
	public void evaluate (IntegerLiteralExp ile) throws WellFormednessException {
		DataType t = uf.findDataTypeByName("Integer");
		if (t == null) throw new WellFormednessException(ile,WellFormednessException.EC_NOT_EXISTS_TYPE);
		ile.setType(t);
	}
	/** Never call directly. Use {@link #typecheck typecheck} instead. */
	public void evaluate (RealLiteralExp rle) throws WellFormednessException {
		Type t = uf.findDataTypeByName("Real");
		if (t == null) throw new WellFormednessException(rle,WellFormednessException.EC_NOT_EXISTS_TYPE);
		rle.setType(t);
	}
	/** Never call directly. Use {@link #typecheck typecheck} instead. */
	public void evaluate (BooleanLiteralExp ble) throws WellFormednessException {
		Type t = uf.findDataTypeByName("Boolean");
		if (t == null) throw new WellFormednessException(ble,WellFormednessException.EC_NOT_EXISTS_TYPE);
		ble.setType(t);
	}
	/** Never call directly. Use {@link #typecheck typecheck} instead. */
	public void evaluate (StringLiteralExp sle) throws WellFormednessException {
		Type t = uf.findDataTypeByName("String");
		if (t == null) throw new WellFormednessException(sle,WellFormednessException.EC_NOT_EXISTS_TYPE);
		sle.setType(t);
	}
	
	
	/*========================*
	 * Collection Literal Exp *
	 *========================*/
	
	 /** Never call directly. Use {@link #typecheck typecheck} instead. 
	 * @throws AttrEvalException */    
    //evaluate the type of a CollectionLiteralExp  
    public void evaluate(CollectionLiteralExp exp) throws AttrEvalException{
        CollectionKind kind = exp.getKind();
        if(kind==null){
            throw new WellFormednessException(exp, WellFormednessException.EC_NO_COLLECTIONKIND);
        }
        
        //the element type of the CollectionLiteralExp is the common supertype of its parts
        Type type = null;
        Type elementType = null;
       
        Iterator it = exp.getPart().iterator();
        while(it.hasNext()){
            CollectionLiteralPart p =  (CollectionLiteralPart) it.next();
            if (elementType == null) elementType = ut.getCorrectType(p);
            else {
            	elementType = this.commonSuperType(elementType, ut.getCorrectType(p));
            }
        }
        if(kind == CollectionKindEnum.SET)			{ type = ut.newCollectionType("Set", elementType); }
        if(kind == CollectionKindEnum.BAG)			{ type = ut.newCollectionType("Bag", elementType); }
        if(kind == CollectionKindEnum.SEQUENCE)		{ type = ut.newCollectionType("Sequence", elementType); }
        if(kind == CollectionKindEnum.ORDERED_SET)	{ type = ut.newCollectionType("OrderedSet", elementType); }
        
        exp.setType(type);
    }

	
	/** Never call directly. Use {@link #typecheck typecheck} instead. **/   
    //the type of a colection range is always integer. the following method just checks, if 
    // the start value and end value of the range are integers as well
    public void evaluate(CollectionRange cr) throws AttrEvalException{
        OclExpression first = cr.getFirst();
        if(first==null){
            throw new WellFormednessException(cr, WellFormednessException.EC_COLL_RANGE_NO_FIRST);
        }
        OclExpression last = cr.getLast();
        if(last==null){
            throw new WellFormednessException(cr, WellFormednessException.EC_COLL_RANGE_NO_LAST);
        }
       
        Type intType = uf.findDataTypeByName("Integer");
        Type typeFirst = this.typecheck(first);
        Type typeLast = this.typecheck(last);

        if(!typeFirst.equals(intType) || !typeLast.equals(intType)){
            throw new WellFormednessException(cr, WellFormednessException.EC_COLL_RANGE_INT);
        }
        
        // Special case in order to protect if the expression range is a PropertyCallExp with
        // collection type (The known problem of type in PCExp)
        if (first instanceof PropertyCallExp) {
        	if (ut.hasCollectionType((PropertyCallExp) first)) {
        		throw new WellFormednessException(cr, WellFormednessException.EC_COLL_RANGE_INT);
        	}
        }
        if (last instanceof PropertyCallExp) {
        	if (ut.hasCollectionType((PropertyCallExp) last)) {
        		throw new WellFormednessException(cr, WellFormednessException.EC_COLL_RANGE_INT);
        	}
        }
        
        cr.setType(intType);
    }
    
    /** Never call directly. Use {@link #typecheck typecheck} instead. */    
    //evaluate the type of a CollectionItem by considering the referred expression
    public void evaluate(CollectionItem ci) throws AttrEvalException {
        OclExpression item = ci.getItem();
        if(item == null){
            throw new WellFormednessException(ci, WellFormednessException.EC_NO_COLLECTION_ITEM);
        }
        this.typecheck(item);
        Type t = ut.getCorrectType(item);
        ci.setType(t);
    }
    
    /** Never call directly. Use {@link #typecheck typecheck} instead. 
     * @throws ConstraintException */ 
    //the type of a TupleLiteralExp is a tuple type comprising the names and types of the tuple parts.
    public void evaluate(TupleLiteralExp exp) throws WellFormednessException, ConstraintException{ 
    	TupleType tt = (TupleType) this.factory.createNode("TupleType");
        String name = "TupleType(";
        String tlename = "Tuple{";
        Property p;
        
    	Iterator it = exp.getPart().iterator();
        while(it.hasNext()){
            TupleLiteralPart tlp = (TupleLiteralPart) it.next();
            p = tlp.getAttribute();
            p.setUmlclass(tt);
            name += ""+p.getName()+":"+p.getType().getName()+",";
            tlename+=""+p.getName()+":"+p.getType().getName()+"="+tlp.getValue().getName()+",";
        }
        if (name.endsWith(",")) {
        	name = name.substring(0, name.length()-1);
        	tlename = tlename.substring(0, tlename.length()-1);
        }
        name += ")";
        tlename += "}";
        tt.setName(name);
        exp.setType(tt);
        exp.setName(tlename);
    }
	
	
	/*=======================*
	 * Operation Expressions *
	 *=======================*/
	/** Never call directly. Use {@link #typecheck typecheck} instead. */
	public void evaluate (Operation op) throws WellFormednessException {
		// the operation must have a type (only for arithmetic operations)
		throw new WellFormednessException((TypedElement) op, WellFormednessException.EC_NOT_EXISTS_TYPE);
	}
	
	
	
	/*==================*
	 * Auxiliar Methods *
	 *==================*/
	/**
	 * Method for the evaluation of an arithmetic or logic operation
	 * @param esq the left side OclExpression
	 * @param op the operator of the binary operation
	 * @param dre the right side OclExpression
	 * @return the correct type of the binary operation, or null
	 * @throws AttrEvalException
	 */
	private Type evaluateArithmeticAndLogicBinaryOpCall (OclExpression left, Operation op, OclExpression right) throws AttrEvalException {
		// The return type
		Type t = null;

		Type tleft = typecheck(left);
		tleft = ut.getCorrectType(left);
		
		Type tright = null;
		if (right != null) {
			tright = typecheck(right);
			tright = ut.getCorrectType(right);
		}
		
		if (left instanceof PropertyCallExp && ut.computeResultTypeOfNavigation(left)==ut.SET_INDIVIDUAL) {
			tleft = ((PropertyCallExp) left).getReferredProperty().getType();
		}
		
		if (right instanceof PropertyCallExp && ut.computeResultTypeOfNavigation(right)==ut.SET_INDIVIDUAL) {
			tright = ((PropertyCallExp) right).getReferredProperty().getType();
		}
		
		// left expression must not be a Collection (unless the operation is '=')
		if (tleft instanceof CollectionType && !op.getName().equals("=")) {
			throw new AttrEvalException("Operation '"+op.getName()+"' cannot be used with a collection source "+tleft.getName()+".");
		}
		// right expression must not be a Collection (unless the operation is '=')
		if (tright instanceof CollectionType && !op.getName().equals("=")) {
			throw new AttrEvalException("Operation '"+op.getName()+"' cannot be used with a collection source "+tright.getName()+".");
		}
		
		// left expression must not be a Tuple (unless the operation is '=')
		if (tleft instanceof TupleType && !op.getName().equals("=")) {
			throw new AttrEvalException("Operation '"+op.getName()+"' cannot be used with a tuple source "+tleft.getName()+".");
		}
		// right expression must not be a Tuple (unless the operation is '=')
		if (tright instanceof TupleType && !op.getName().equals("=")) {
			throw new AttrEvalException("Operation '"+op.getName()+"' cannot be used with a tuple source "+tright.getName()+".");
		}
		
		if (tright instanceof Enumeration && !(relationalops.contains(op.getName()))) {
			throw new AttrEvalException("Operation '"+op.getName()+"' cannot be used with a enumeration source "+tright.getName()+".");
		}
		
		if (tleft instanceof Enumeration && !(relationalops.contains(op.getName()))) {
			throw new AttrEvalException("Operation '"+op.getName()+"' cannot be used with a enumeration source "+tleft.getName()+".");
		}
		
		// Case 1. Arithmetic Operation
		if (aritmeticops.contains(op.getName())) {
			t = CheckArithmetic(left, op, right);
		}
		// Case 2. Logical Operation
		else if (logicalops.contains(op.getName())) {
			t = CheckLogical(left, op, right);
		}
		// Case 3. Relational Operation
		else if (relationalops.contains(op.getName())) {
			t = CheckRelational(left, op, right);
		}
		// Undefined Case. Error (it will never arrive at this point)
		else {
			throw new AttrEvalException("This error must not appear.");
		}
		
		return t;
	}
	/**
	 * Method for evaluate the type of a collection operation 
	 * @param source the source expression
	 * @param op the operation
	 * @param params the operation parameters
	 * @return the correct type of the collection operation
	 * @throws AttrEvalException
	 * @throws ConstraintException 
	 */
	private Type evaluateCollectionOpCall (OclExpression source, Operation op, Collection params) throws AttrEvalException, ConstraintException {
		Type t = null;
		if (source==null) {
			throw new AttrEvalException("Operation "+op.getName()+" has no source");
		}
		Type sourcetype = typecheck(source);
		Type elementType = null;
		int resulttype = ut.ERROR; // By default
		
		// pce representing a navigation to an associationEnd -> is a CollectionType
		if (source instanceof PropertyCallExp) {
			PropertyCallExp pce = (PropertyCallExp) source;
			resulttype = ut.computeResultTypeOfNavigation(pce);
			if (verbose) System.out.println("Collection type for PCE in collection operation: "+resulttype);
			if (!ut.hasCollectionType((PropertyCallExp) source))
				throw new AttrEvalException("Operation "+op.getName()+" needs a CollectionType as source (PCE type error)");
			elementType = pce.getType();
		}// the source expression must be a Collection
		else if (sourcetype instanceof CollectionType) {
			elementType = ((CollectionType)sourcetype).getElementType();
		}
		else {
			throw new AttrEvalException("Operation "+op.getName()+" needs a CollectionType as source");
		}
	
		String opname = op.getName();
		
		// =====================
		// Case 1: no parameters
		if (params.isEmpty()) {
			// SIZE
			if (opname.equals("size")) {
				t = uf.findDataTypeByName("Integer");
			}// IS_EMPTY NOT_EMPTY
			else if (opname.equals("isEmpty") || opname.equals("notEmpty")) {
				t = uf.findDataTypeByName("Boolean");
			}// SUM
			else if (opname.equals("sum")) {
				if (elementType.getName().equals("Integer") || elementType.getName().equals("Real")) {
					t = elementType;
				}
				else throw new AttrEvalException("Semantic Error: sum() operation is not aplicable to these collection elements");
			}// FLATTEN (Set, Bag or Sequence)
			else if (opname.equals("flatten")) {
				// case PCE
				if (resulttype == ut.SET_INDIVIDUAL 
					|| resulttype == ut.BAG
					|| resulttype == ut.SET_MULTIPLE
					|| resulttype == ut.SEQUENCE) {
					t = ut.createTypeForCollectionPCE(resulttype, elementType);
				}
				// case Collection
				else if (sourcetype instanceof SetType || sourcetype instanceof BagType || sourcetype instanceof SequenceType) {
					if (elementType instanceof CollectionType) {
						elementType = ((CollectionType)elementType).getElementType();
						t = ut.newCollectionType((CollectionType) sourcetype, elementType);
					} else {
						t = sourcetype; 
					}
				} else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Set, Bag or Sequence.");
				}
			}// AS_SET (Set, Bag or Sequence)
			else if (opname.equals("asSet")) {
				if (resulttype == ut.SET_INDIVIDUAL
					|| resulttype == ut.SET_MULTIPLE 
					|| resulttype == ut.BAG
					|| resulttype == ut.SEQUENCE) {
					t = ut.createTypeForCollectionPCE(ut.SET_MULTIPLE, elementType);
				}else if (sourcetype instanceof SetType 
						  || sourcetype instanceof BagType 
						  || sourcetype instanceof SequenceType) {
					t = ut.newCollectionType("Set", elementType);
				}
				else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Set, Bag or Sequence.");
				}
			}// AS_ORDEREDSET (Set, Bag or Sequence)
			else if (opname.equals("asOrderedSet")) {
				if (resulttype == ut.SET_INDIVIDUAL
					|| resulttype == ut.SET_MULTIPLE 
					|| resulttype == ut.BAG
					|| resulttype == ut.SEQUENCE) {
					t = ut.createTypeForCollectionPCE(ut.ORDEREDSET, elementType);
				}else if (sourcetype instanceof SetType 
					|| sourcetype instanceof BagType 
					|| sourcetype instanceof SequenceType) {
					t = ut.newCollectionType("OrderedSet", elementType);
				}
				else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Set, Bag or Sequence.");
				}
			}// AS_SEQUENCE (Set, Bag or Sequence)
			else if (opname.equals("asSequence")) {
				if (resulttype == ut.SET_INDIVIDUAL
					|| resulttype == ut.SET_MULTIPLE 
					|| resulttype == ut.BAG
					|| resulttype == ut.SEQUENCE) {
					t = ut.createTypeForCollectionPCE(ut.SEQUENCE, elementType);
				}else if (sourcetype instanceof SetType 
					|| sourcetype instanceof BagType 
					|| sourcetype instanceof SequenceType) {
					t = ut.newCollectionType("Sequence", elementType);
				}
				else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Set, Bag or Sequence.");
				}
			}// AS_BAG (Set, Bag or Sequence)
			else if (opname.equals("asBag")) {
				if (resulttype == ut.SET_INDIVIDUAL
					|| resulttype == ut.SET_MULTIPLE 
					|| resulttype == ut.BAG
					|| resulttype == ut.SEQUENCE) {
					t = ut.createTypeForCollectionPCE(ut.BAG, elementType);
				}else if (sourcetype instanceof SetType 
					|| sourcetype instanceof BagType 
					|| sourcetype instanceof SequenceType) {
					t = ut.newCollectionType("Bag", elementType);
				}
				else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Set, Bag or Sequence.");
				}	
			}// FIRST LAST (OrderedSet or Sequence)
			else if (opname.equals("first") || opname.equals("last")) {
				if (resulttype == ut.ORDEREDSET || resulttype == ut.SEQUENCE ) {
					t = elementType;
				}else if (sourcetype instanceof OrderedSetType || sourcetype instanceof SequenceType) {
						t = elementType;
				}else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be OrderedSet or Sequence.");
				}
			}// incorrect matching between opname and number of parameters, or incorrect operation
			else {
				throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+".");	
			}
		}
		// =====================
		// Case 2: only one parameter
		else if (params.size() == 1) {
			// param contains the parameter
			OclExpression param = (OclExpression) (params.toArray())[0];
			
			Type paramType;
			if (param instanceof PropertyCallExp) {
				if (ut.hasCollectionType((PropertyCallExp)param)) {
					paramType = ut.createTypeForCollectionPCE(ut.computeResultTypeOfNavigation(param), param.getType());
				}
				else paramType = param.getType();
			}
			else paramType = param.getType();
			
			if (paramType == null) throw new AttrEvalException("Semantic Error: the parameter on "+opname+" does not have type.");
			
			// INCLUDES EXCLUDES
			if (opname.equals("includes") || opname.equals("excludes")) {
				if (existsCompatibility(elementType,paramType)) {
					t = uf.findDataTypeByName("Boolean");
				}
				else {
					throwIncompatibilityError(opname,source,paramType);
				}
			} // COUNT
			else if (opname.equals("count")) {
				if (existsCompatibility(elementType,paramType)) {
					t = uf.findDataTypeByName("Integer");
				}
				else {
					throwIncompatibilityError(opname,source,paramType);
				}
			} // INCLUDES_ALL EXCUDES_ALL
			else if (opname.equals("includesAll") || opname.equals("excludesAll")) {
				if (paramType instanceof CollectionType) {
					Type elementOfParamCollection = ((CollectionType)paramType).getElementType();
					if (existsCompatibility(elementType, elementOfParamCollection)) {
						t = uf.findDataTypeByName("Boolean");
					}
					else {
						throwIncompatibilityError(opname,source,paramType);
					}
				}
				else throw new AttrEvalException("Semantic Error: "+opname+" operation needs a collection as a parameter");
			} // PRODUCT
			else if (opname.equals("product")) {
				if (!(paramType instanceof CollectionType))
					throw new AttrEvalException("Semantic Error: the parameter on "+opname+" is not a Collection. It is a "+paramType.getName());
				
				Type elementOfParamCollection = ((CollectionType)paramType).getElementType();
				
				SetType st = (SetType) factory.createNode("SetType");
				TupleType tt = (TupleType) factory.createNode("TupleType");
				// elements of the tupletype
				Property first = (Property) factory.createNode("Property");
				Property second = (Property) factory.createNode("Property");
				first.setName("first");
				second.setName("second");
				first.setType(elementType);
				second.setType(elementOfParamCollection);
				
				first.setUmlclass(tt);
				second.setUmlclass(tt);
				
				tt.setName("TupleType(first:"+first.getType().getName()+", second:"+second.getType().getName()+")");
				st.setName("Set("+tt.getName()+")");
				st.setElementType(tt);
				t = st;
			} // UNION (Set, Bag or Sequence)
			else if (opname.equals("union")) {
				if (paramType instanceof SetType || paramType instanceof BagType) {
					Type elementOfParamCollection = ((CollectionType)paramType).getElementType();
					if (!existsCompatibility(elementType, elementOfParamCollection)) {
						throwIncompatibilityError(opname,source,paramType);
					}
					if (resulttype == ut.SET_MULTIPLE) {
						t = ut.newCollectionType((CollectionType)paramType, elementType);
					}
					else if (resulttype == ut.BAG) {
						t = ut.newCollectionType("Bag", elementType);
					}
					else if (sourcetype instanceof SetType) {
						t = ut.newCollectionType((CollectionType)paramType, elementType);
					}
					else if (sourcetype instanceof BagType) {
						t = sourcetype;
					}
					else {
						throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Set, Bag or Sequence.");
					}
				}
				else if (paramType instanceof SequenceType) {
					if (!(sourcetype instanceof SequenceType)) {
						throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Set, Bag or Sequence.");
					}
					Type elementOfParamCollection = ((CollectionType)paramType).getElementType();
					if (!existsCompatibility(elementType, elementOfParamCollection)) {
						throwIncompatibilityError(opname,source,paramType);
					}
					t = sourcetype;
				}
				else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". The parameter must be Set, Bag or Sequence.");
				}	
			}// INTERSECTION (Set or Bag)
			else if (opname.equals("intersection")) {
				if (!(paramType instanceof SetType || paramType instanceof BagType)) {
					throw new AttrEvalException("Semantic Error: the parameter on "+opname+" is not a Set or Bag. It is a "+paramType.getName());
				}
				Type elementOfParamCollection = ((CollectionType)paramType).getElementType();
				if (resulttype == ut.SET_MULTIPLE 
					|| resulttype == ut.BAG) {
					if (existsCompatibility(elementType, elementOfParamCollection)) {
						t = ut.createTypeForCollectionPCE(resulttype, elementType);
					}
					else {
						throwIncompatibilityError(opname,source,paramType);
					}
				}else if (sourcetype instanceof SetType 
					|| sourcetype instanceof BagType 
					|| sourcetype instanceof SequenceType) {
					if (existsCompatibility(elementType, elementOfParamCollection)) {
						t = sourcetype;
					}
					else {
						throwIncompatibilityError(opname,source,paramType);
					}
				}
				else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Set, Bag or Sequence.");
				}	
			}// INCLUDING EXCLUDING (Set, Bag or Sequence)
			else if (opname.equals("including") || opname.equals("excluding")) {
				if (resulttype == ut.SET_MULTIPLE 
					|| resulttype == ut.BAG
					|| resulttype == ut.SEQUENCE) {
					if (existsCompatibility(elementType, paramType)) {
						t = ut.createTypeForCollectionPCE(resulttype, elementType);
					}
					else {
						throwIncompatibilityError(opname,source,paramType);
					}
				}else if (sourcetype instanceof SetType 
					|| sourcetype instanceof BagType 
					|| sourcetype instanceof SequenceType) {
					if (existsCompatibility(elementType, paramType)) {
						t = sourcetype;
					}
					else {
						throwIncompatibilityError(opname,source,paramType);
					}
				}
				else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Set, Bag or Sequence.");
				}	
			}// SYMMETRIC_DIFFERENCE (Set)
			else if (opname.equals("symmetricDifference")) {
				if (!(paramType instanceof SetType))
					throw new AttrEvalException("Semantic Error: the parameter on "+opname+" is not a Set. It is a "+paramType.getName());
				Type elementOfParamCollection = ((CollectionType)paramType).getElementType();
				if (resulttype == ut.SET_MULTIPLE) {
					if (existsCompatibility(elementType, elementOfParamCollection))
						t = ut.createTypeForCollectionPCE(resulttype, elementType);
					else {
						throwIncompatibilityError(opname,source,paramType);
					}
				} else if (sourcetype instanceof SetType) {
					if (existsCompatibility(elementType, elementOfParamCollection))
						t = sourcetype;
					else {
						throwIncompatibilityError(opname,source,paramType);
					}
				} else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Set.");
				}
			}// APPEND PREPEND (OrderedSet or Sequence)
			else if (opname.equals("append") || opname.equals("prepend")) {
				if (resulttype == ut.ORDEREDSET || resulttype == ut.SEQUENCE) {
					if (existsCompatibility(elementType, paramType))
						t = ut.createTypeForCollectionPCE(resulttype, elementType);
					else {
						throwIncompatibilityError(opname,source,paramType);
					}
				} else if (sourcetype instanceof OrderedSetType || sourcetype instanceof SequenceType) {
					if (existsCompatibility(elementType, paramType))
						t = sourcetype;
					else {
						throwIncompatibilityError(opname,source,paramType);
					}
				} else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Sequence.");
				}
			}// AT (OrderedSet or Sequence)
			else if (opname.equals("at")) {
				if (!paramType.getName().equals("Integer")) 
					throw new AttrEvalException("Semantic Error: the parameter on "+opname+" is not Integer.");
				if (resulttype == ut.ORDEREDSET || resulttype == ut.SEQUENCE) {
					t = elementType;
				}else if (sourcetype instanceof OrderedSetType || sourcetype instanceof SequenceType) {
					t = elementType;
				}
				else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Set, Bag or Sequence.");
				}
			}// INDEX_OF (OrderedSet or Sequence)
			else if (opname.equals("indexOf")) {
				if (source instanceof PropertyCallExp) {
					if (!(resulttype == ut.ORDEREDSET || resulttype == ut.SEQUENCE)) 
						throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be OrderedSet or Sequence.");
				}
				else if (!(sourcetype instanceof OrderedSetType || sourcetype instanceof SequenceType)) {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be OrderedSet or Sequence.");
				}
				if (existsCompatibility(elementType,paramType)) {
					t = uf.findDataTypeByName("Integer");
				}
				else {
					throwIncompatibilityError(opname,source,paramType);
				}
			}// NOT_IN ñ (Set)
			else if (opname.equals("ñ")) {
				if (!(paramType instanceof SetType))
					throw new AttrEvalException("Semantic Error: the parameter on "+opname+" is not a Set. It is a "+paramType.getName());
				Type elementOfParamCollection = ((CollectionType)paramType).getElementType();
				if (resulttype == ut.SET_MULTIPLE) {
					if (existsCompatibility(elementType, elementOfParamCollection))
						t = ut.createTypeForCollectionPCE(resulttype, elementType);
					else {
						throwIncompatibilityError(opname,source,paramType);
					}
				} else if (sourcetype instanceof SetType) {
					if (existsCompatibility(elementType, elementOfParamCollection))
						t = sourcetype;
					else {
						throwIncompatibilityError(opname,source,paramType);
					}
				} else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Set.");
				}
			}// incorrect matching between opname and number of parameters, or incorrect operation
			else {
				throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+".");
			}
		}
		// =====================
		// Case 3: two parameters
		else if (params.size() == 2) {
			OclExpression param1 = (OclExpression) (params.toArray())[1];
			Type param1Type, param2Type;
			if (param1 instanceof PropertyCallExp) {
				if (ut.hasCollectionType((PropertyCallExp)param1)) {
					param1Type = ut.createTypeForCollectionPCE(ut.computeResultTypeOfNavigation(param1), param1.getType());
				}
				else param1Type = param1.getType();
			}
			else param1Type = param1.getType();
			
			OclExpression param2 = (OclExpression) (params.toArray())[0];
			if (param2 instanceof PropertyCallExp) {
				if (ut.hasCollectionType((PropertyCallExp)param2)) {
					param2Type = ut.createTypeForCollectionPCE(ut.computeResultTypeOfNavigation(param2), param2.getType());
				}
				else param2Type = param2.getType();
			}
			else param2Type = param2.getType();
			
			if (param1Type == null) throw new AttrEvalException("Semantic Error: the first parameter on "+opname+" does not have type.");
			if (param2Type == null) throw new AttrEvalException("Semantic Error: the second parameter on "+opname+" does not have type.");
			
			// INSERT_AT (OrderedSet or Sequence)
			if (opname.equals("insertAt")) {
				if (!param1Type.getName().equals("Integer")) 
					throw new AttrEvalException("Semantic Error: the first parameter on "+opname+" is not Integer.");
				if (!existsCompatibility(elementType, param2Type)) 
					throw new AttrEvalException("Semantic Error: the second parameter on "+opname+" is not Integer.");
				if (resulttype == ut.ORDEREDSET || resulttype == ut.SEQUENCE) {
					t = ut.createTypeForCollectionPCE(resulttype, elementType);
				} else if (sourcetype instanceof OrderedSetType || sourcetype instanceof Sequence) {
					t = sourcetype;
				} else {
					throwIncompatibilityError(opname,source,param2Type);
				}
			}// SUB_ORDERED_SET (OrderedSet)
			else if (opname.equals("subOrderedSet")) {
				if (!param1Type.getName().equals("Integer")) 
					throw new AttrEvalException("Semantic Error: the first parameter on "+opname+" is not Integer.");
				if (!param2Type.getName().equals("Integer")) 
					throw new AttrEvalException("Semantic Error: the second parameter on "+opname+" is not Integer.");
				if (resulttype == ut.ORDEREDSET) {
					t = ut.createTypeForCollectionPCE(resulttype, elementType);
				} else if (sourcetype instanceof OrderedSetType) {
					t = sourcetype;
				} else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be OrderedSet.");
				}
			}// SUB_SEQUENCE (Sequence)
			else if (opname.equals("subSequence")) {
				if (!param1Type.getName().equals("Integer")) 
					throw new AttrEvalException("Semantic Error: the first parameter on "+opname+" is not Integer.");
				if (!param2Type.getName().equals("Integer")) 
					throw new AttrEvalException("Semantic Error: the second parameter on "+opname+" is not Integer.");
				if (resulttype == ut.SEQUENCE) {
					t = ut.createTypeForCollectionPCE(resulttype, elementType);
				} else if (sourcetype instanceof SequenceType) {
					t = sourcetype;
				} else {
					throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+". Source must be Sequence.");
				}
			}// incorrect matching between opname and number of parameters, or incorrect operation
			else {
				throw new AttrEvalException("Semantic Error: incorrect usage of "+opname+".");
			}
		}
		// =====================
		// Case 4: other situations
		else {
			throw new AttrEvalException("Semantic Error: incorrect usage of "+opname);
		}
	
		return t;
	}
	
	public boolean existsCompatibility(Type t, Type compatible) throws AttrEvalException {
		if (t.equals(compatible)) return true;
		else {
			if (t.getName().equals(compatible.getName())) return true;
			if (t instanceof CollectionType) {
				if (compatible instanceof CollectionType) {
					if (ut.haveSameCollectionKind(t, compatible)) {
						Type elementType1 = ((CollectionType)t).getElementType();
						Type elementType2 = ((CollectionType)compatible).getElementType();
						
						if (elementType1!=null && elementType2!=null)
							return existsCompatibility(elementType1, elementType2);
						else if (elementType1==null && elementType2==null) return true;
						else if (elementType1!=null && elementType2==null) return true;
						else return false;
					}
					else return false;
				}
				else return false;
			}
			else if (t.equals(uf.findDataTypeByName("Real"))) {
				if (compatible.equals(uf.findDataTypeByName("Integer"))) return true;
				else return false;
			}
			else if (t instanceof TupleType) {
				if (compatible instanceof TupleType) {
					return existsTupleCompatibility((TupleType)t, (TupleType)compatible);
				}
				else return false;
			}
			else if (t instanceof UmlClass) {
				if (compatible instanceof UmlClass) {
					if (ut.isSubClass((UmlClass)t,(UmlClass)compatible)) {
						return true;
					}
					else return false;
				}
				else return false;
			}
			else return false;
		}
	}
	

	private boolean existsTupleCompatibility(TupleType t, TupleType compatible) throws AttrEvalException {
		List members1 = t.getOwnedAttribute();
		List members2 = compatible.getOwnedAttribute();
		boolean exists = false;
		
		if (members1.size()==members2.size()) {
			for (Iterator iterator = members1.iterator(); iterator.hasNext();) {
				Property attributeOf1 = (Property) iterator.next();
				exists = false;
				for (Iterator iterator2 = members2.iterator(); iterator2.hasNext() && !exists;) {
					Property attributeOf2 = (Property) iterator2.next();
					if (attributeOf1.getName().equals(attributeOf2.getName())) {
						exists = true;
						if (!existsCompatibility(attributeOf1.getType(),attributeOf2.getType()) &&
							!existsCompatibility(attributeOf2.getType(),attributeOf1.getType())) {
							throw new AttrEvalException("Incompatibility of types " +
									"in the comparison of two TupleTypes found at attribute "+attributeOf1.getName()+".");
						}
					}
				}//for2
				if (!exists) {
					throw new AttrEvalException("Only one TupleType in the " +
							"comparison has an attribute with the name "+attributeOf1.getName()+".");
				}
			}//for1
			return true;
		}
		else {
			throw new AttrEvalException("Incompatibility of TupleTypes:" +
					" different number of elements ("+members1.size()+" and "+members2.size()+").");
		}
	}

	/**
	 * Method for evaluate the type of a relational operation
	 * @param left the left expression
	 * @param op the operation
	 * @param right the right expression
	 * @return the type of the operation expression
	 * @throws AttrEvalException
	 */
	private Type CheckRelational(OclExpression left, Operation op, OclExpression right) throws AttrEvalException {
		Type t = null; // The return type
		Type tbool = uf.findDataTypeByName("Boolean");
		
		Type tleft = typecheck(left);
		Type tright = typecheck(right);
		
		// Case 1. Operation equal (=) or distinct (<>)
		// For these operations, if the types are equal then boolean type is returned
		if (op.getName().equals("=")) {
			// Collection and Tuple comparison is possible
			boolean delete_tleft = false;
			boolean delete_tright = false;
			
			if (right instanceof PropertyCallExp && left instanceof PropertyCallExp) {
				PropertyCallExp pleft = (PropertyCallExp) left;
				PropertyCallExp pright = (PropertyCallExp) right;
				int resultright = ut.computeResultTypeOfNavigation(pright);
				int resultleft = ut.computeResultTypeOfNavigation(pleft);
				
				if (resultright == resultleft && this.existsCompatibility(pleft.getType(), pright.getType())) {
					return tbool;
				}
				else throwError(op.getName(), ut.getNameOfResultTypeOfNavigation(pleft)+
						" and "+ut.getNameOfResultTypeOfNavigation(pright));
			}
			
			
			if (left instanceof PropertyCallExp) {
				PropertyCallExp pce = (PropertyCallExp) left;
				int resulttype = ut.computeResultTypeOfNavigation(pce);
				if (resulttype != ut.ERROR && resulttype != ut.ATTRIBUTE && resulttype != ut.SET_INDIVIDUAL) {
					tleft = ut.createTypeForCollectionPCE(resulttype, pce.getType());
					delete_tleft = true;
				}
			}
			if (right instanceof PropertyCallExp && tleft instanceof CollectionType) {
				PropertyCallExp pce = (PropertyCallExp) right;
				int resulttype = ut.computeResultTypeOfNavigation(pce);
				if (resulttype != ut.ERROR && resulttype != ut.ATTRIBUTE) {
					tright = ut.createTypeForCollectionPCE(resulttype, pce.getType());
					delete_tright = true;
				}
			}
			if (right instanceof PropertyCallExp && !(tleft instanceof CollectionType)) {
				System.out.println("Pasamos correctamente");
				PropertyCallExp pce = (PropertyCallExp) right;
				int resulttype = ut.computeResultTypeOfNavigation(pce);
				if (resulttype != ut.ERROR && resulttype != ut.ATTRIBUTE && resulttype != ut.SET_INDIVIDUAL) {
					tright = ut.createTypeForCollectionPCE(resulttype, pce.getType());
					delete_tright = true;
				}
			}
			
			
			if (tleft.getName().equals(tright.getName())) { 
				t = tbool;
				if (delete_tleft) tleft.refDelete();
				if (delete_tright) tright.refDelete();
			}
			else if (this.existsCompatibility(tleft, tright)) { 
				t = tbool;
				if (delete_tleft) tleft.refDelete();
				if (delete_tright) tright.refDelete();
			}
			else if (this.existsCompatibility(tright, tleft)) { 
				t = tbool;
				if (delete_tleft) tleft.refDelete();
				if (delete_tright) tright.refDelete();
			}
			else throwError(op.getName(), tleft.getName()+" and "+tright.getName());
		} 
		else if ( op.getName().equals("<>")) {
			// Case 1.1. Expression types are not null
			if (tleft != null && tright != null) {
				// Equal types ok, different types->error
				if (tleft.equals(tright)) t = tbool;
				else throwError(op.getName(), tleft.getName()+" and "+tright.getName());
			}
			else // type is needed
				throw new AttrEvalException("Operation "+op.getName()+" with at least one operand without type.");
		}
		// Case 2. Operations <, <=, >, >=
		else {
			// Case 2.1. Expression types are not null
			if (tleft != null && tright != null) {
				// Case 2.1.1. Expression types are equal
				if (tleft.equals(tright)) {
					// Types are Integer or Real -> return Boolean
					if (tleft.getName().equals("Integer")|| tleft.getName().equals("Real"))
						t = tbool;
					else if (tleft instanceof Enumeration) t = tbool;
					else throwError(op.getName(), tleft.getName());
				}
				// Case 2.1.2. Expression types are different
				else {
					// Types are integer and real, or real and integer -> return Boolean
					if (implicitConversionIntToReal(tleft, tright))
						t = tbool;
					else throwError(op.getName(), tleft.getName()+" and "+tright.getName());
				}
			}
			// Case 2. Right type is null
			else if (tright == null) {
				// Integer or Real -> ok
				if (tleft.getName().equals("Integer") || tleft.getName().equals("Real"))
					t = tbool;
				else throwError(op.getName(), tleft.getName());
			}
			// Case 3. Left type is null
			else if (tleft == null) {
				// Integer or Real -> ok
				if (tright.getName().equals("Integer") || tright.getName().equals("Real"))
					t = tbool;
				else throwError(op.getName(), tright.getName());
			}
			// Case 4. The two types are null
			else {
				// By default, return Boolean
				t = tbool;
			}
		}
		return t;
	}
	/**
	 * Method for evaluate the type of a logical operation
	 * @param left the left expression
	 * @param op the operation
	 * @param right the right expression
	 * @return the type of the operation expression
	 * @throws AttrEvalException
	 */
	private Type CheckLogical(OclExpression left, Operation op, OclExpression right) throws AttrEvalException {
		Type t = null; // The return type
		
		Type tleft = typecheck(left);
		Type tright = null;
		if (right != null) tright = typecheck(right);
		
		// Case 1. Expression types are not null
		if (tleft != null && tright != null) {
			// Case 1.1. Expression types are equal
			if (tleft.equals(tright)) {
				// Boolean ok, other->error
				if (tleft.getName().equals("Boolean"))
					//CCE t = tleft;
					t = uf.findDataTypeByName(tleft.getName());
				else throwError(op.getName(), tleft.getName());
			}
			// Case 1.2. Expression types are different
			else throwError(op.getName(), tleft.getName()+" and "+tright.getName());
		}
		// Case 2. Right type is null
		else if (tright == null) {
			// Boolean ok, other->error
			if (tleft.getName().equals("Boolean"))
				//CCE t = tleft;
				t = uf.findDataTypeByName(tleft.getName());
			else throwError(op.getName(), tleft.getName());
		}
		// Case 3. Left type is null
		else if (tleft == null) {
			// Boolean ok, other->error
			if (tright.getName().equals("Boolean"))
				//CCE t = tright;
				t = uf.findDataTypeByName(tright.getName());
			else throwError(op.getName(), tright.getName());			
		}
		// Case 4. The two types are null
		else {
			// By default, return Boolean
			t = uf.findDataTypeByName("Boolean");
		}
		return t;
	}
	/**
	 * Method for evaluate the type of an arithmetic operation
	 * @param left the left expression
	 * @param op the operation
	 * @param right the right expression
	 * @return the type of the operation expression
	 * @throws AttrEvalException
	 */
	private Type CheckArithmetic(OclExpression left, Operation op, OclExpression right) throws AttrEvalException {
		Type t = null; // The return type
		
		Type tleft = typecheck(left);
		Type tright = null; // tright could be null if the operation is unary minus (-)
		if (right != null) tright = typecheck(right);
		
		// Case 1. Expression types are not null
		if (tleft != null && tright != null) {
			// Case 1.1. Expression types are equal
			if (tleft.equals(tright)) {
				// Case 1.1.1. Types are Integer or Real -> return one of them
				if (tleft.getName().equals("Integer")|| tleft.getName().equals("Real"))
					//CCE t = tleft;
					t = uf.findDataTypeByName(tleft.getName());
				else throwError(op.getName(), tleft.getName());
			}
			// Case 1.2. Expression types are different
			else {
				// Case 1.2.1. Types are integer and real, or real and integer -> return Real
				if (implicitConversionIntToReal(tleft, tright))
					t = uf.findDataTypeByName("Real");
				else throwError(op.getName(), tleft.getName()+" and "+tright.getName());
			}
		}
		// Case 2. Right type is null
		else if (tright == null) {
			// Integer or Real -> ok
			if (tleft.getName().equals("Integer") || tleft.getName().equals("Real"))
				//CCE t = tleft;
				t = uf.findDataTypeByName(tleft.getName());
			else throwError(op.getName(), tleft.getName());
		}
		// Case 3. Left type is null
		else if (tleft == null) {
			// Integer or Real -> ok
			if (tright.getName().equals("Integer") || tright.getName().equals("Real"))
				//CCE t = tright;
				t = uf.findDataTypeByName(tright.getName());
			else throwError(op.getName(), tright.getName());
		}
		// Case 4. The two types are null
		else {
			// By default, return Integer
			t = uf.findDataTypeByName("Integer");
		}
		return t; 
	}
	/**
	 * Indicate whether a implicit conversion from integer to real is possible  
	 * @param tleft the left type
	 * @param tright the right type
	 * @return true if the left type is real and the right one is integer
	 */
	private boolean implicitConversionIntToReal(Type tleft, Type tright) {
		if (verbose) System.out.println("conversio implicita d'enter a real");
		// we obtain the integer and real types
		Type tint = uf.findDataTypeByName("Integer");
		Type treal = uf.findDataTypeByName("Real");
		
		// left is real and right is integer -> OK
		if (tleft.equals(treal) && tright.equals(tint)) return true;
		// right is real and left is integer -> OK
		else if (tleft.equals(tint) && tright.equals(treal)) return true;
		else return false;
	}
	
	/**
	 * Method for make easier throw an AttrEvalException 
	 * @param msg the message to throw in the Exception
	 * @throws AttrEvalException
	 */
	private void throwError (String msg, String tipus) throws AttrEvalException {
		throw new AttrEvalException ("Incompatibility of types: operation '"+msg+"' with "
				+ tipus+ " expressions.");
	}
	private void throwIncompatibilityError(String opname, OclExpression source, Type paramType) throws AttrEvalException {
		String nameParamType = paramType.getName();
		String nameSourceType;
		if (source instanceof PropertyCallExp) 
			nameSourceType = ut.getNameOfResultTypeOfNavigation((PropertyCallExp) source);
		else nameSourceType = source.getType().getName();
		throw new AttrEvalException("Semantic Error: "+opname+" -> incompatibility of types " +
				"between parameter ("+nameParamType+") and source ("+nameSourceType+")");
	}
    private Type commonSuperType(Type t1, Type t2) throws AttrEvalException {
    	// CHANGE: this is provisional
    	if (t1.equals(t2)) return t1;
    	else if ((t1.getName().equals("Integer") && t2.getName().equals("Real"))    ||
    			 (t1.getName().equals("Real")    && t2.getName().equals("Integer"))
    			) 
    			return uf.findDataTypeByName("Real");
    	else if (this.existsCompatibility(t1, t2)) return t1;
    	else if (this.existsCompatibility(t2, t1)) return t2;
    	throw new AttrEvalException("Incompatibility of types: "+t1.getName()+" and "+t2.getName());
    	
    }
    
    public boolean isCollectionOp(String name) {
    	if (this.collectops.contains(name)) return true;
    	else return false;
    }
    public boolean isAdditionalOp(String name) {
    	if (this.additionalops.contains(name)) return true;
    	else return false;
    }
    public boolean isOtherBasicOp(String name) {
    	if (this.aritmeticops.contains(name)) return true;
    	if (this.logicalops.contains(name)) return true;
    	if (this.relationalops.contains(name)) return true;
    	return false;
    }

	
    
}
